/*
 * RPrApp.cpp
 *
 *  Created on: May 26, 2012
 *      Author: kobe
 */

#include "RPrApp.h"

R_PrApp::R_PrApp(Agent* agent, Proposition* prop, Proposition* propprime) {
	this->mAgent = agent;
	this->mProp = prop;
	this->mPropPrime = propprime;
	mIsSimplified = false;
}

R_PrApp::R_PrApp(Agent* agent, Proposition* prop, Proposition* propprime, bool simplified) {
	this->mAgent = agent;
	this->mProp = prop;
	this->mPropPrime = propprime;
	mIsSimplified = true;
}

R_PrApp::~R_PrApp() {
	// TODO Auto-generated destructor stub
}
std::vector<Sequent*> R_PrApp::run(Sequent* s) {
	std::vector<Sequent*> result;
	std::string str(s->toString());
	//std::cout << "input sequent:" << str << std::endl;
	Sequent* duplicate = new Sequent(str);
	Context* context = duplicate->getContext();
	Proposition* prop = duplicate->getProposition();
	Context* target = search(context);
	if (target == NULL) {
		//std::cout << "Target is null" << std::endl;
		return result;
	} else {
		std::vector<Agent*> agentList = target->getAgentList();
		Agent* agent = agentList.front();
		std::vector<Context*> items = target->getItemList();
		for (std::vector<Context*>::iterator i = items.begin(); i < items.end();
				i++) {
			Context* ctx = *i;
			if (ctx->getType() == CONTEXT_PROPOSITION) {
				Proposition* p = ctx->getProposition();
				if (p->getPropName() == ATOMIC && p->compare(mProp)) {

					if (checkLoop(target, mPropPrime)) {
						return result;
					}
					items.erase(i);
					target->setItemList(items);
					break;
				}
			}
		}
		//replace target by new context
		//potential memory leak
		Context* np = new Context(mPropPrime->toString());
		Context* nc = new Context(target->toString());
		std::vector<Context*> list;
		list.push_back(np);
		if (target->getItemList().size() > 0) {
			list.push_back(nc);
		}
		std::vector<Agent*> alist;
		target->setAgentList(alist);
		target->setItemList(list);
		result.push_back(duplicate);
		return result;
	}
}

bool R_PrApp::checkLoop(Context* context, Proposition* p) {
	Context* parent = context->getParent();
	int count = 0;
	if (parent == NULL)
		return false;
	std::vector<Context*> items = parent->getItemList();
	for (size_t i = 0; i < items.size(); i++) {
		if (items[i]->getType() == CONTEXT_PROPOSITION
				&& items[i]->getProposition()->compare(p)) {
			count++;
		}
	}
	if (count >= 1) {
		return true;
	}
	return false;
}

Context* R_PrApp::search(Context* context) {
	Context* result = NULL;
	std::vector<Agent*> agentList = context->getAgentList();
	if (agentList.size() > 0) {
		//check the innermost one
		Agent* agent = agentList.front();
		if (agent->compare(mAgent)) {
			if (context->getType() == PROPOSITIONCONTEXT) {
				std::vector<Context*> items = context->getItemList();
				for (int i = 0; i < items.size(); i++) {
					Context* ctx = items[i];
					if (ctx->getType() == CONTEXT_PROPOSITION) {
						if (ctx->getProposition()->getPropName() == ATOMIC
								&& ctx->getProposition()->compare(mProp)) {
							return context;
						}
					}
				}
			}
		} else {
			return NULL;
		}
	}
	//No luck this level. Go one step deeper
	std::vector<Context*> items = context->getItemList();
	for (int i = 0; i < items.size(); i++) {
		result = search(items[i]);
		if (result != NULL) {
			return result;
		}
	}
	return result;
}

std::string R_PrApp::toString() {
	std::string s("Rule: PrApp");
	return s;
}

std::string R_PrApp::toLatex() {
	std::string s(" PrApp(");
	s += mAgent->toLatex();
	s += ",";
	s += mProp->toLatex();
	s += ",";
	s += mPropPrime->toLatex();
	s += ")";
	return s;
}

RuleType R_PrApp::getRuleType() {
	return PRAPP;
}

